use std::{
    collections::{BTreeMap, HashSet},
    sync::{Arc, Mutex},
};

use async_recursion::async_recursion;
use tokio::sync::MutexGuard;
use varisat::{ExtendFormula, Lit, Solver};

use crate::solve::TransationState;

use super::{SolveContext, SolvePkgInfo};
use anyhow::Result;
impl SolveContext {
    pub async fn solve(&self) -> Result<()> {
        let mut formula_lock = self.formula.lock().await;
        let assume_lock = self.assume.lock().await;
        let mut assume = HashSet::new();
        for ele in assume_lock.conflict_installed.iter() {
            assume.insert(*ele);
        }
        for ele in assume_lock.necessary.iter() {
            assume.insert(*ele);
        }
        for ele in assume_lock.installed.iter() {
            assume.insert(*ele);
        }
        let mut entry_req_lock = self.entry_require.lock().await;
        for (solve_item, (entry_index, pkg_infos)) in entry_req_lock.iter_mut() {
            pkg_infos.sort();
            let mut lits = pkg_infos
                .iter()
                .map(|x| Lit::from_dimacs(x.pkg_index))
                .collect::<Vec<_>>();
            if pkg_infos.len() == 0 {
                dbg!(solve_item);
            }
            lits.push(!Lit::from_dimacs(*entry_index));
            formula_lock.add_clause(&lits);
        }

        let same_pkg_lock = self.same_pkg_name.lock().await;
        // for (pkg_name, index_set) in same_pkg_lock.iter() {
        //     let index_vec = index_set.iter().collect::<Vec<_>>();
        //     if pkg_name == "perl-libs" {
        //         continue;
        //     }
        //     if index_vec.len() >= 2 {
        //         for head in 0..index_vec.len() - 1 {
        //             for tail in (head + 1)..index_vec.len() {
        //                 formula_lock.add_clause(&[
        //                     !Lit::from_dimacs(index_vec[head].abs()),
        //                     !Lit::from_dimacs(index_vec[tail].abs()),
        //                 ]);
        //             }
        //         }
        //     }
        // }
        drop(same_pkg_lock);

        let assume = assume
            .iter()
            .map(|x| Lit::from_dimacs(*x as isize))
            .collect::<Vec<_>>();
        let mut solver = Solver::new();

        solver.add_formula(&formula_lock);
        solver.assume(&assume);
        let pkginfos = self.index_map_pkginfo.lock().await;
        // pkginfos.clone();
        let mut pkg_infos = BTreeMap::new();
        for (pkg_index, pkg_info) in pkginfos.iter() {
            pkg_infos.insert(*pkg_index, (*pkg_info).to_owned());
        }
        let appeared = Vec::new();
        self.clone()
            .solve_assume(Arc::new(Mutex::new(solver)), assume, pkg_infos, appeared)?;
        Ok(())
    }
    // #[async_recursion]
    fn solve_assume(
        self,
        solver: Arc<Mutex<Solver>>,
        assume: Vec<Lit>,
        pkginfos: BTreeMap<isize, SolvePkgInfo>,
        mut appeared: Vec<Lit>,
    ) -> Result<()> {
        let mut solver_lock = solver.lock().unwrap();
        solver_lock.assume(&assume);
        if solver_lock.solve()? {
            // let pkginfos = self.index_map_pkginfo.lock();
            let mut to_install = Vec::new();
            let mut to_upgrade = Vec::new();
            match solver_lock.model() {
                Some(v) => {
                    for ele in v {
                        if let Some(p) = pkginfos.get(&(ele.to_dimacs().abs())) {
                            if ele.is_positive() {
                                match p.state {
                                    TransationState::ToInstall => {
                                        if let Some(_s) = self
                                            .installed_repo
                                            .data
                                            .clone()
                                            .get_pkg_uuid_by_pkg_name(p.pkg_name.clone())
                                        {
                                            to_upgrade.push(p);
                                        } else {
                                            to_install.push(p);
                                        };
                                    }
                                    TransationState::Upgrade => {
                                        to_upgrade.push(p);
                                    }
                                    _ => {}
                                }
                            }
                        };
                    }
                }
                None => {}
            }
            to_install.sort_by(|a, b| a.pkg_name.cmp(&b.pkg_name));
            to_upgrade.sort_by(|a, b| a.pkg_name.cmp(&b.pkg_name));
            let to_install_name = to_install
                .iter()
                .map(|x| x.pkg_name.as_str())
                .collect::<Vec<_>>();
            let to_upgrade_name = to_upgrade
                .iter()
                .map(|x| x.pkg_name.as_str())
                .collect::<Vec<_>>();
            dbg!(to_install_name);
            dbg!(to_upgrade_name);
        } else {
            dbg!("error");
            // for ele in formula_lock.iter() {
            //     if ele.len() <= 1 {
            //         // dbg!(ele);
            //         let index = &ele[0].to_dimacs().abs();
            //         if let Some(s) = self.index_map_pkginfo.lock().await.get(&index) {
            //             dbg!(s);
            //         };
            //         if let Some(s) = self.index_map_entry.lock().await.get(index) {
            //             dbg!(s);
            //         }
            //         if let Some(s) = self.index_map_term.lock().await.get(index) {
            //             dbg!(s);
            //         }
            //     }
            // }
            match solver_lock.failed_core() {
                Some(s) => {
                    // dbg!(s);
                    // for ele in s {
                    let mut res = false;
                    for ele in s {
                        if !appeared.contains(ele) {
                            appeared.push(*ele);
                        } else {
                            res = true;
                        }
                    }
                    if res {
                        let assume = assume
                            .iter()
                            .filter(|x| !s.contains(*x))
                            .map(|x| *x)
                            .collect::<Vec<_>>();
                        self.clone()
                            .solve_assume(solver.clone(), assume, pkginfos, appeared)?;
                    }

                    // let index = ele.to_dimacs();
                    // if let Some(s) = self.index_map_pkginfo.lock().await.get(&index) {
                    //     dbg!(s);
                    // };
                    // if let Some(s) = self.index_map_entry.lock().await.get(&index) {
                    //     dbg!(s);
                    // }
                    // if let Some(s) = self.index_map_term.lock().await.get(&index) {
                    //     dbg!(s);
                    // }
                    // }

                    // for index in s {
                    //     let mut assume = HashSet::new();
                    //     for ele in assume_lock.conflict_installed.iter() {
                    //         assume.insert(*ele);
                    //     }
                    //     for ele in assume_lock.necessary.iter() {
                    //         assume.insert(*ele);
                    //     }
                    //     for ele in assume_lock.installed.iter() {
                    //         if index.to_dimacs().abs() != *ele {
                    //             assume.insert(*ele);
                    //         }
                    //     }
                    // }
                }
                None => {}
            }
            // let p = solver.model().unwrap();
            // dbg!(p);
            // solver.config(config_update);
        };
        Ok(())
    }
}
#[cfg(test)]
mod tests {
    // use crate::Rdnf;
    #[test]
    fn test_set() {
        let v = vec![0, 1, 2];
        // let index_vec = index_set.iter().collect::<Vec<_>>();
        // for head in 0..index_vec.len() - 1 {
        //     for tail in head..index_vec.len() {
        //         formula_lock.add_clause(&[
        //             !Lit::from_dimacs(*index_vec[head]),
        //             !Lit::from_dimacs(*index_vec[tail]),
        //         ]);
        //     }
        // }
        for head in 0..v.len() - 1 {
            for tail in (head + 1)..v.len() {
                dbg!(vec![v[head], v[tail]]);
            }
        }
    }
    // async fn new_context() {
    //     let _repos = Rdnf::make_cache(
    //         self.repo_confs,
    //         self.conf.config_main.clone(),
    //         self.cli,
    //         self.term,
    //     )
    //     .await?;
    //     let installed_repo =
    //         InstalledRepo::open(&self.conf.config_main, DEFAULT_RPMDB_LOCATION).await?;
    // }
}
